Iof proof for Lemma inv image ind:
A:Type, r:(A
A
), B:Type, f:(BA).
WellFnd{i}(A;x,y.r(x,y)) 
WellFnd{i}(B;x,y.r(f(x),f(y)))
by Lemma `inv_image_ind_tp`
.| 9,38 |
A:Type, r:(AA), B:Type, f:(BA).
WellFnd{i}(A;x,y.r(x,y)) WellFnd{i}(B;x,y.r(f(x),f(y)))
by Lemma `inv_image_ind_tp`
.
| Lemmas |